COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	αx subj     bring tp to sail
C00008 00003	αx subj     hard copy
C00011 00004	compiling at sail see THM.ALL
C00012 00005	THM.EXE may be created by typing:
C00013 00006	α⊃  to get THM
C00017 00007	9jun84 making and  testing bmp  aliased to [bmp,sys]
C00021 00008	α⊃  to get THM
C00022 00009	αx sl bmp
C00023 ENDMK
C⊗;
;αx subj     bring tp to sail

retr AUX:<CL.THM>Code.Tags
retr -This-.-Dir-← aux:<cl.thm>-This-.-Dir-
retr -READ-.-THIS-←aux:<cl.thm>-READ-.-THIS-
retr AUX:<CL.THM>Thm.All
retr aux:<cl.thm>COMPLR.INI
retr thmlsp.ini←aux:<cl.thm>lisp.ini
retr aux:<cl.thm>basis.lisp
retr aux:<cl.thm>crock1.lsp
retr aux:<cl.thm>genfact.lisp
retr aux:<cl.thm>crock2.lsp
retr aux:<cl.thm>events.lisp
retr aux:<cl.thm>crock3.lsp
retr code-1-a.lisp←aux:<cl.thm>code-1-a.lisp
retr code-b-d.lisp←aux:<cl.thm>code-b-d.lisp
retr code-e-m.lisp←aux:<cl.thm>code-e-m.lisp
retr code-n-r.lisp←aux:<cl.thm>code-n-r.lisp
retr code-s-z.lisp←aux:<cl.thm>code-s-z.lisp
retr aux:<cl.thm>io.lisp
retr aux:<cl.thm>ppr.lisp
retr make-thm.lisp←aux:<cl.thm>make-thm.lisp


retr AUX:<CL.PROOFS>XXXS.LISP
retr aux:<cl.thm>code.doc
retr <CL.TP2>CODE.DOC
retr <CL.TP2>CODE.TXT

;retr AUX:<CL.PROOFS>PROVEALL.LIB
;retr AUX:<CL.PROOFS>PROVEALL.LISP
;retr BOOT-STRAP.LIB←AUX:<CL.PROOFS>BOOT-STRAP.LIB
;< File not accessable. No such filename

retr aux:<cl.thm>code.doc
Writing CODE.DOC[BMP,SYS]
< ASCII retrieve of AUX:<CL.THM>CODE.DOC.5 started.
< Transfer completed.
Input complete: 9299 bytes transferred (10.8 Kbaud)
*
retr oldcod.doc←aux:<CL.TP2>CODE.DOC
< ASCII retrieve of AUX:<CL.TP2>CODE.DOC.7907 started.
< Transfer completed.
Input complete: 132941 bytes transferred (8.2 Kbaud)
*
retr aux:<CL.TP2>CODE.TXT
Writing CODE.TXT[BMP,SYS]
< ASCII retrieve of AUX:<CL.TP2>CODE.TXT.2 started.
< Transfer completed.
Input complete: 5630 bytes transferred (6.5 Kbaud)
*
;αx subj     hard copy

boise Code.Tag

boise ↓-THIS-↓.↓-DIR-↓

boise ↓-READ-↓.↓-THIS-↓

boise THM.ALL

boise COMPLR.INI

boise lisp.ini

boise basis.lisp

boise CROCK1.LSP

boise GENFAC.LIS

boise CROCK2.LSP

boise EVENTS.LIS

boise CROCK3.LSP

boise ↓CODE-1-A↓.LISP
boise ↓CODE-B-D↓.LISP
boise ↓CODE-E-M↓.LISP
boise ↓CODE-N-R↓.LISP
boise ↓CODE-S-Z↓.LISP

boise IO.LIS
boise PPR.LIS
boise ↓MAKE-THM↓.LISP

----

boise PROVEALL.LIB
boise PROVEALL.LISP

boise XXXS.LISP

boise ↓BOOT-STRAP↓.LIB
boise ↓BOOT-STRAP↓.LISP

boise code.doc[bmp,sys]
boise oldcod.doc[bmp,sys]
boise CODE.TXT[bmp,sys]

;compiling at sail see THM.ALL
;αx subj
; complr.ini sets base, and removes match-macro autoload

r bcomplr


;CD AUX:<CL.THM>
;PS:<MACLISP>COMPLR

BASIS.LISP(u,w)
;; loads basis.fasl
CROCK1.LSP(u)

GENFACT.LISP(u,w)
;; loads genfact.fasl
CROCK2.LSP(u)

EVENTS.LISP(u,w)
;; loads events.fasl
CROCK3.LSP(u)
CODE-1-A.LISP(u,w)
CODE-B-D.LISP(u,w)
CODE-E-M.LISP(u,w)
CODE-N-R.LISP(u,w)
CODE-S-Z.LISP(u,w)

IO.LISP(u,w)
PPR.LISP(u,w)
MAKE-THM.LISP(u,w)

;TOPS-20-EMACS-TO-THM.LISP

THM.EXE may be created by typing:

	@MACLISP AUX:<CL.THM>LISP.INI
	*(MAKE-THM)
        @SAVE THM.EXE 0 777

POOR is the online file for the current user's manual. 

XXXS.LISP contains our standard benchmark.

do mkthm
;;α⊃  to get THM

In checking out the change to NOTE-LIB, I suggest that, after making the
change, you perform:

(BOOT-STRAP)
[ 4.088 0.0 ]
GROUND-ZERO 

(MAKE-LIB "FOO")
(#FILE-OUT-|DSK:FOO.LIB[BM,CLT]|-71774 #FILE-OUT-|DSK:FOO.LIS[BM,CLT]|-71770) 

(NOTE-LIB "FOO.LIB" "FOO.LISP")
#FILE-IN-|DSK:FOO.LIB[BM,CLT]|-71764 

(ASSOC-OF-APPEND)
January 15, 1984  21:23:2
(DEFN APPEND
      (X Y)
      (IF (LISTP X)
	  (CONS (CAR X) (APPEND (CDR X) Y))
	  Y))
     Linear arithmetic and the lemma CDR-LESSP inform us that the
measure (COUNT X) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, APPEND is accepted under the
principle of definition.  Observe that:
      (OR (LISTP (APPEND X Y))
	  (EQUAL (APPEND X Y) Y))
is a theorem.



[ 1.34599991 0.06299998 ]
APPEND 
(PROVE-LEMMA ASSOC-OF-APPEND
	     (REWRITE)
	     (EQUAL (APPEND (APPEND A B) C)
		    (APPEND A (APPEND B C))))
     Give the conjecture the name *1.

     Let us appeal to the induction principle.  The recursive terms
in the conjecture suggest three inductions.  They merge into two
likely candidate inductions.  However, only one is unflawed.  We will
induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP A) (P (CDR A) B C))
		    (P A B C))
	   (IMPLIES (NOT (LISTP A)) (P A B C))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT A) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme
generates two new conjectures:
Case 2. (IMPLIES (AND (LISTP A)
		      (EQUAL (APPEND (APPEND (CDR A) B) C)
			     (APPEND (CDR A) (APPEND B C))))
		 (EQUAL (APPEND (APPEND A B) C)
			(APPEND A (APPEND B C)))),
  which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
  unfolding APPEND, to:
        T.
Case 1. (IMPLIES (NOT (LISTP A))
		 (EQUAL (APPEND (APPEND A B) C)
			(APPEND A (APPEND B C)))),
  which simplifies, expanding the definition of APPEND, to:
        T.

     That finishes the proof of *1.  Q.E.D.

[ 0.773999915 0.208000056 ]
ASSOC-OF-APPEND 
(APPEND ASSOC-OF-APPEND) 

;;9jun84 making and  testing bmp  aliased to [bmp,sys]
;;  r plisp
;; (load "bmp.mk")
;; (make-thm)
;; save neutp 
;; baby tests  - see below

;; ren bmp.dmp[1,3]←neubmp.dmp
;; r bmp
;; (load "provea.eve")

(BOOT-STRAP)
[ 4.43299997 0.0 ]
GROUND-ZERO 

(MAKE-LIB "FOO")
(#FILE-OUT-|DSK:FOO.LIB[1,CLT]|-71770 #FILE-OUT-|DSK:FOO.LIS[1,CLT]|-71766) 

(NOTE-LIB "FOO.LIB" "FOO.LISP")
#FILE-IN-|DSK:FOO.LIB[1,CLT]|-71762 

;(ASSOC-OF-APPEND)
(DEFN APPEND
      (X Y)
      (IF (LISTP X)
	  (CONS (CAR X) (APPEND (CDR X) Y))
	  Y))
     Linear arithmetic and the lemma CDR-LESSP inform us that the
measure (COUNT X) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, APPEND is accepted under the
principle of definition.  Observe that:
      (OR (LISTP (APPEND X Y))
	  (EQUAL (APPEND X Y) Y))
is a theorem.



[ 1.35 0.06299998 ]
APPEND 

(PROVE-LEMMA ASSOC-OF-APPEND
	     (REWRITE)
	     (EQUAL (APPEND (APPEND A B) C)
		    (APPEND A (APPEND B C))))
     Give the conjecture the name *1.

     Let us appeal to the induction principle.  The recursive terms
in the conjecture suggest three inductions.  They merge into two
likely candidate inductions.  However, only one is unflawed.  We will
induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP A) (P (CDR A) B C))
		    (P A B C))
	   (IMPLIES (NOT (LISTP A)) (P A B C))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT A) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme
generates two new conjectures:
Case 2. (IMPLIES (AND (LISTP A)
		      (EQUAL (APPEND (APPEND (CDR A) B) C)
			     (APPEND (CDR A) (APPEND B C))))
		 (EQUAL (APPEND (APPEND A B) C)
			(APPEND A (APPEND B C)))),
  which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
  unfolding APPEND, to:
        T.
Case 1. (IMPLIES (NOT (LISTP A))
		 (EQUAL (APPEND (APPEND A B) C)
			(APPEND A (APPEND B C)))),
  which simplifies, expanding the definition of APPEND, to:
        T.

     That finishes the proof of *1.  Q.E.D.

[ 0.77899996 0.20500005 ]
ASSOC-OF-APPEND 
;;α⊃  to get THM

boot-strap
proveall  1hr:16min   (1:54 realtime)
rsa  45min
wilson
 
αx sl bmp
(load "provea.eve")